0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 AND
↳5 IDP
↳6 IDPtoQDPProof (⇒)
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 YES
↳14 IDP
↳15 IDPtoQDPProof (⇒)
↳16 QDP
↳17 UsableRulesProof (⇔)
↳18 QDP
↳19 QReductionProof (⇔)
↳20 QDP
↳21 QDPSizeChangeProof (⇔)
↳22 YES
↳23 IDP
↳24 IDPNonInfProof (⇒)
↳25 IDP
↳26 IDependencyGraphProof (⇔)
↳27 TRUE
public class Entry
{
private String item;
private int count;
public Entry(String itemData, int countData)
{
item = itemData;
count = countData;
}
public String toString( )
{
return (item + " " + count);
}
public boolean equals(Object otherObject)
{
if (otherObject == null)
return false;
else if (getClass( ) != otherObject.getClass( ))
return false;
else
{
Entry otherEntry = (Entry)otherObject;
return (item.equals(otherEntry.item)
&& (count == otherEntry.count));
}
}
// <There should be other constructors and methods, including accessor and
// mutator methods, but we do not use them in this demonstration.>
}
public class LinkedList<T>
{
private class Node<T>
{
private T data;
private Node<T> link;
public Node( )
{
data = null;
link = null;
}
public Node(T newData, Node<T> linkValue)
{
data = newData;
link = linkValue;
}
}//End of Node<T> inner class
private Node<T> head;
public LinkedList( )
{
head = null;
}
/**
Adds a node at the start of the list with the specified data.
The added node will be the first node in the list.
*/
public void addToStart(T itemData)
{
this.head = new Node<T>(itemData, this.head);
}
/**
Removes the head node and returns true if the list contains at least
one node. Returns false if the list is empty.
*/
public boolean deleteHeadNode( )
{
if (head != null)
{
head = head.link;
return true;
}
else
return false;
}
/**
Returns the number of nodes in the list.
*/
public int size( )
{
int count = 0;
Node<T> position = head;
while (position != null)
{
count++;
position = position.link;
}
return count;
}
public boolean contains(T item)
{
return (find(item) != null);
}
/**
Finds the first node containing the target item, and returns a
reference to that node. If target is not in the list, null is returned.
*/
private Node<T> find(T target)
{
Node<T> position = head;
T itemAtPosition;
while (position != null)
{
itemAtPosition = position.data;
if (itemAtPosition.equals(target))
return position;
position = position.link;
}
return null; //target was not found
}
/**
Finds the first node containing the target and returns a reference
to the data in that node. If target is not in the list, null is returned.
*/
public T findData(T target)
{
return find(target).data;
}
public void outputList( )
{
Node<T> position = head;
while (position != null)
{
//System.out.println(position.data);
position = position.link;
}
}
public boolean isEmpty( )
{
return (head == null);
}
public void clear( )
{
head = null;
}
/*
For two lists to be equal they must contain the same data items in
the same order. The equals method of T is used to compare data items.
*/
public boolean equals(Object otherObject)
{
if (!(otherObject instanceof LinkedList))
return false;
else
{
LinkedList<T> otherList = (LinkedList<T>)otherObject;
if (size( ) != otherList.size( ))
return false;
Node<T> position = head;
Node<T> otherPosition = otherList.head;
while (position != null)
{
if (!(position.data.equals(otherPosition.data)))
return false;
position = position.link;
otherPosition = otherPosition.link;
}
return true; //no mismatch was not found
}
}
public static void main(String[] args)
{
LinkedList<Entry> list = new LinkedList<Entry>( );
for (int i = 1; i < args.length; i++) {
Entry entry = new Entry(args[i], i++);
list.addToStart(entry);
entry = new Entry(args[i], i++);
list.addToStart(entry);
entry = new Entry(args[i], i++);
list.addToStart(entry);
}
list.size(); // remove it!
//System.out.println("List has " + list.size( )
// + " nodes.");
list.outputList( );
//System.out.println("End of list.");
}
}
Generated 28 rules for P and 10 rules for R.
Combined rules. Obtained 5 rules for P and 1 rules for R.
Filtered ground terms:
3455_0_outputList_NULL(x1, x2, x3) → 3455_0_outputList_NULL(x2, x3)
LinkedList$Node(x1, x2) → LinkedList$Node(x2)
3807_0_access$000_Return(x1, x2) → 3807_0_access$000_Return(x2)
3775_0_access$000_Return(x1, x2) → 3775_0_access$000_Return(x2)
3546_0_outputList_Return(x1) → 3546_0_outputList_Return
Filtered duplicate args:
3455_0_outputList_NULL(x1, x2) → 3455_0_outputList_NULL(x2)
Finished conversion. Obtained 5 rules for P and 1 rules for R. System has no predefined symbols.
Generated 29 rules for P and 11 rules for R.
Combined rules. Obtained 5 rules for P and 1 rules for R.
Filtered ground terms:
3573_0_size_NULL(x1, x2, x3) → 3573_0_size_NULL(x2, x3)
LinkedList$Node(x1, x2) → LinkedList$Node(x2)
4030_0_access$000_Return(x1, x2) → 4030_0_access$000_Return(x2)
3998_0_access$000_Return(x1, x2) → 3998_0_access$000_Return(x2)
3608_0_size_Return(x1) → 3608_0_size_Return
Filtered duplicate args:
3573_0_size_NULL(x1, x2) → 3573_0_size_NULL(x2)
Finished conversion. Obtained 5 rules for P and 1 rules for R. System has no predefined symbols.
Generated 140 rules for P and 170 rules for R.
Combined rules. Obtained 1 rules for P and 0 rules for R.
Filtered ground terms:
4281_0_main_Load(x1, x2, x3, x4, x5) → 4281_0_main_Load(x2, x3, x4, x5)
LinkedList$Node(x1) → LinkedList$Node
LinkedList(x1, x2) → LinkedList(x2)
Cond_4281_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_4281_0_main_Load(x1, x3, x4, x5, x6)
Filtered duplicate args:
4281_0_main_Load(x1, x2, x3, x4) → 4281_0_main_Load(x1, x2, x4)
Cond_4281_0_main_Load(x1, x2, x3, x4, x5) → Cond_4281_0_main_Load(x1, x2, x3, x5)
Combined rules. Obtained 1 rules for P and 0 rules for R.
Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
(0) -> (1), if ((3775_0_access$000_Return(x0[0]) →* 3775_0_access$000_Return(x0[1]))∧(java.lang.Object(LinkedList$Node(x0[0])) →* java.lang.Object(LinkedList$Node(x0[1]))))
(1) -> (0), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[0]))))
(1) -> (2), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[2]))))
(1) -> (3), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[3]))))
(2) -> (0), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[0]))))
(2) -> (2), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[2]'))))
(2) -> (3), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[3]))))
(3) -> (4), if ((3807_0_access$000_Return(x0[3]) →* 3807_0_access$000_Return(x0[4]))∧(java.lang.Object(LinkedList$Node(x0[3])) →* java.lang.Object(LinkedList$Node(x0[4]))))
(4) -> (0), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[0]))))
(4) -> (2), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[2]))))
(4) -> (3), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[3]))))
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3455_0_OUTPUTLIST_NULL(x0[1])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3455_0_OUTPUTLIST_NULL(x0[2])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3455_0_OUTPUTLIST_NULL(x0[4])
3455_0_outputList_NULL(NULL) → 3546_0_outputList_Return
3455_0_outputList_NULL(NULL)
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3455_0_OUTPUTLIST_NULL(x0[1])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3455_0_OUTPUTLIST_NULL(x0[2])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3455_0_OUTPUTLIST_NULL(x0[4])
3455_0_outputList_NULL(NULL)
3455_0_outputList_NULL(NULL)
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3775_1_OUTPUTLIST_INVOKEMETHOD(3775_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3455_0_OUTPUTLIST_NULL(x0[1])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3455_0_OUTPUTLIST_NULL(x0[2])
3455_0_OUTPUTLIST_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
3807_1_OUTPUTLIST_INVOKEMETHOD(3807_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3455_0_OUTPUTLIST_NULL(x0[4])
From the DPs we obtained the following set of size-change graphs:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
(0) -> (1), if ((3998_0_access$000_Return(x0[0]) →* 3998_0_access$000_Return(x0[1]))∧(java.lang.Object(LinkedList$Node(x0[0])) →* java.lang.Object(LinkedList$Node(x0[1]))))
(1) -> (0), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[0]))))
(1) -> (2), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[2]))))
(1) -> (3), if ((x0[1] →* java.lang.Object(LinkedList$Node(x0[3]))))
(2) -> (0), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[0]))))
(2) -> (2), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[2]'))))
(2) -> (3), if ((x0[2] →* java.lang.Object(LinkedList$Node(x0[3]))))
(3) -> (4), if ((4030_0_access$000_Return(x0[3]) →* 4030_0_access$000_Return(x0[4]))∧(java.lang.Object(LinkedList$Node(x0[3])) →* java.lang.Object(LinkedList$Node(x0[4]))))
(4) -> (0), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[0]))))
(4) -> (2), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[2]))))
(4) -> (3), if ((x0[4] →* java.lang.Object(LinkedList$Node(x0[3]))))
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3573_0_SIZE_NULL(x0[1])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3573_0_SIZE_NULL(x0[2])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3573_0_SIZE_NULL(x0[4])
3573_0_size_NULL(NULL) → 3608_0_size_Return
3573_0_size_NULL(NULL)
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3573_0_SIZE_NULL(x0[1])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3573_0_SIZE_NULL(x0[2])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3573_0_SIZE_NULL(x0[4])
3573_0_size_NULL(NULL)
3573_0_size_NULL(NULL)
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[0]))) → 3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[0]), java.lang.Object(LinkedList$Node(x0[0])))
3998_1_SIZE_INVOKEMETHOD(3998_0_access$000_Return(x0[1]), java.lang.Object(LinkedList$Node(x0[1]))) → 3573_0_SIZE_NULL(x0[1])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[2]))) → 3573_0_SIZE_NULL(x0[2])
3573_0_SIZE_NULL(java.lang.Object(LinkedList$Node(x0[3]))) → 4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[3]), java.lang.Object(LinkedList$Node(x0[3])))
4030_1_SIZE_INVOKEMETHOD(4030_0_access$000_Return(x0[4]), java.lang.Object(LinkedList$Node(x0[4]))) → 3573_0_SIZE_NULL(x0[4])
From the DPs we obtained the following set of size-change graphs:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(0) -> (1), if ((x3[0] > 1 && x3[0] < x0[0] && x0[0] > x3[0] + 1 && x0[0] > x3[0] + 1 + 1 && 3 < x3[0] + 1 + 1 →* TRUE)∧(java.lang.Object(ARRAY(x0[0], x1[0])) →* java.lang.Object(ARRAY(x0[1], x1[1])))∧(java.lang.Object(LinkedList(x2[0])) →* java.lang.Object(LinkedList(x2[1])))∧(x3[0] →* x3[1]))
(1) -> (0), if ((java.lang.Object(ARRAY(x0[1], x1[1])) →* java.lang.Object(ARRAY(x0[0], x1[0])))∧(java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))) →* java.lang.Object(LinkedList(x2[0])))∧(x3[1] + 1 + 1 + 1 + 1 →* x3[0]))
(1) (&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1)))=TRUE∧java.lang.Object(ARRAY(x0[0], x1[0]))=java.lang.Object(ARRAY(x0[1], x1[1]))∧java.lang.Object(LinkedList(x2[0]))=java.lang.Object(LinkedList(x2[1]))∧x3[0]=x3[1] ⇒ 4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])≥NonInfC∧4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])≥COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])∧(UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥))
(2) (<(3, +(+(x3[0], 1), 1))=TRUE∧>(x0[0], +(+(x3[0], 1), 1))=TRUE∧>(x0[0], +(x3[0], 1))=TRUE∧>(x3[0], 1)=TRUE∧<(x3[0], x0[0])=TRUE ⇒ 4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])≥NonInfC∧4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])≥COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])∧(UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥))
(3) (x3[0] + [-2] ≥ 0∧x0[0] + [-3] + [-1]x3[0] ≥ 0∧x0[0] + [-2] + [-1]x3[0] ≥ 0∧x3[0] + [-2] ≥ 0∧x0[0] + [-1] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧[bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]x3[0] + [bni_15]x0[0] ≥ 0∧[1 + (-1)bso_16] ≥ 0)
(4) (x3[0] + [-2] ≥ 0∧x0[0] + [-3] + [-1]x3[0] ≥ 0∧x0[0] + [-2] + [-1]x3[0] ≥ 0∧x3[0] + [-2] ≥ 0∧x0[0] + [-1] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧[bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]x3[0] + [bni_15]x0[0] ≥ 0∧[1 + (-1)bso_16] ≥ 0)
(5) (x3[0] + [-2] ≥ 0∧x0[0] + [-3] + [-1]x3[0] ≥ 0∧x0[0] + [-2] + [-1]x3[0] ≥ 0∧x3[0] + [-2] ≥ 0∧x0[0] + [-1] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧[bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]x3[0] + [bni_15]x0[0] ≥ 0∧[1 + (-1)bso_16] ≥ 0)
(6) (x3[0] + [-2] ≥ 0∧x0[0] + [-3] + [-1]x3[0] ≥ 0∧x0[0] + [-2] + [-1]x3[0] ≥ 0∧x3[0] + [-2] ≥ 0∧x0[0] + [-1] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧0 = 0∧[bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]x3[0] + [bni_15]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)
(7) (x3[0] ≥ 0∧x0[0] + [-5] + [-1]x3[0] ≥ 0∧x0[0] + [-4] + [-1]x3[0] ≥ 0∧x3[0] ≥ 0∧x0[0] + [-3] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]x3[0] + [bni_15]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)
(8) (x3[0] ≥ 0∧x0[0] ≥ 0∧[1] + x0[0] ≥ 0∧x3[0] ≥ 0∧[2] + x0[0] ≥ 0 ⇒ (UIncreasing(COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])), ≥)∧0 = 0∧[(4)bni_15 + (-1)Bound*bni_15] + [bni_15]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)
(9) (COND_4281_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(x2[1])), x3[1])≥NonInfC∧COND_4281_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(x2[1])), x3[1])≥4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))∧(UIncreasing(4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))), ≥))
(10) ((UIncreasing(4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))), ≥)∧[3 + (-1)bso_18] ≥ 0)
(11) ((UIncreasing(4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))), ≥)∧[3 + (-1)bso_18] ≥ 0)
(12) ((UIncreasing(4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))), ≥)∧[3 + (-1)bso_18] ≥ 0)
(13) ((UIncreasing(4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[3 + (-1)bso_18] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(4281_0_MAIN_LOAD(x1, x2, x3)) = [-1]x3 + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(LinkedList(x1)) = [-1]
POL(COND_4281_0_MAIN_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(1) = [1]
POL(<(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(3) = [3]
POL(LinkedList$Node) = [-1]
4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0]) → COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])
COND_4281_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(x2[1])), x3[1]) → 4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1], x1[1])), java.lang.Object(LinkedList(java.lang.Object(LinkedList$Node))), +(+(+(+(x3[1], 1), 1), 1), 1))
4281_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0]) → COND_4281_0_MAIN_LOAD(&&(&&(&&(&&(>(x3[0], 1), <(x3[0], x0[0])), >(x0[0], +(x3[0], 1))), >(x0[0], +(+(x3[0], 1), 1))), <(3, +(+(x3[0], 1), 1))), java.lang.Object(ARRAY(x0[0], x1[0])), java.lang.Object(LinkedList(x2[0])), x3[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer